YES(O(1),O(n^2))
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict Trs:
{ and(tt(), X) -> X
, plus(N, 0()) -> N
, plus(N, s(M)) -> s(plus(N, M))
, x(N, 0()) -> 0()
, x(N, s(M)) -> plus(x(N, M), N) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We use the processor 'custom shape polynomial interpretation' to
orient following rules strictly.
Trs:
{ and(tt(), X) -> X
, plus(N, s(M)) -> s(plus(N, M))
, x(N, s(M)) -> plus(x(N, M), N) }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^2)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
TcT has computed the following constructor-restricted polynomial
interpretation.
[and](x1, x2) = 1 + 3*x1 + 3*x1*x2 + 3*x1^2 + 3*x2
[tt]() = 1
[plus](x1, x2) = x1 + 3*x2
[0]() = 0
[s](x1) = 2 + x1
[x](x1, x2) = x1 + 2*x1*x2 + x2
This order satisfies the following ordering constraints.
[and(tt(), X)] = 7 + 6*X
> X
= [X]
[plus(N, 0())] = N
>= N
= [N]
[plus(N, s(M))] = N + 6 + 3*M
> 2 + N + 3*M
= [s(plus(N, M))]
[x(N, 0())] = N
>=
= [0()]
[x(N, s(M))] = 5*N + 2*N*M + 2 + M
> 4*N + 2*N*M + M
= [plus(x(N, M), N)]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict Trs:
{ plus(N, 0()) -> N
, x(N, 0()) -> 0() }
Weak Trs:
{ and(tt(), X) -> X
, plus(N, s(M)) -> s(plus(N, M))
, x(N, s(M)) -> plus(x(N, M), N) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We use the processor 'custom shape polynomial interpretation' to
orient following rules strictly.
Trs: { plus(N, 0()) -> N }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^2)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
TcT has computed the following constructor-restricted polynomial
interpretation.
[and](x1, x2) = 1 + x1 + x1*x2 + x1^2 + 3*x2
[tt]() = 2
[plus](x1, x2) = 3 + x1 + 2*x2
[0]() = 0
[s](x1) = 1 + x1
[x](x1, x2) = 2*x1 + 2*x1*x2 + 2*x2 + x2^2
This order satisfies the following ordering constraints.
[and(tt(), X)] = 7 + 5*X
> X
= [X]
[plus(N, 0())] = 3 + N
> N
= [N]
[plus(N, s(M))] = 5 + N + 2*M
> 4 + N + 2*M
= [s(plus(N, M))]
[x(N, 0())] = 2*N
>=
= [0()]
[x(N, s(M))] = 4*N + 2*N*M + 3 + 4*M + M^2
>= 3 + 4*N + 2*N*M + 2*M + M^2
= [plus(x(N, M), N)]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict Trs: { x(N, 0()) -> 0() }
Weak Trs:
{ and(tt(), X) -> X
, plus(N, 0()) -> N
, plus(N, s(M)) -> s(plus(N, M))
, x(N, s(M)) -> plus(x(N, M), N) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We use the processor 'custom shape polynomial interpretation' to
orient following rules strictly.
Trs: { x(N, 0()) -> 0() }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^2)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
TcT has computed the following constructor-restricted polynomial
interpretation.
[and](x1, x2) = 1 + 3*x1 + 3*x1*x2 + 3*x1^2 + 3*x2
[tt]() = 1
[plus](x1, x2) = x1 + x2
[0]() = 1
[s](x1) = 1 + x1
[x](x1, x2) = 2*x1 + x1*x2 + x2 + 2*x2^2
This order satisfies the following ordering constraints.
[and(tt(), X)] = 7 + 6*X
> X
= [X]
[plus(N, 0())] = N + 1
> N
= [N]
[plus(N, s(M))] = N + 1 + M
>= 1 + N + M
= [s(plus(N, M))]
[x(N, 0())] = 3*N + 3
> 1
= [0()]
[x(N, s(M))] = 3*N + N*M + 3 + 5*M + 2*M^2
> 3*N + N*M + M + 2*M^2
= [plus(x(N, M), N)]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak Trs:
{ and(tt(), X) -> X
, plus(N, 0()) -> N
, plus(N, s(M)) -> s(plus(N, M))
, x(N, 0()) -> 0()
, x(N, s(M)) -> plus(x(N, M), N) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
Hurray, we answered YES(O(1),O(n^2))